Inference at * 1 1 1 1 2 
Iof proof for Lemma inv image ind a:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. y : S
9. y':S. r(f(y'),f(y))  P(y')
  P(y) 

latex

 by (% Desired main subgoal with inductive hyp 9 % 
((BHyp 7) 
(CollapseTHEN ((Auto_aux (first_nat 
(C1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))) 

latex

(C.

Definitions

t  T, P  Q, x:A. B(x)